#pragma once

#include <vector>
#include <list>
#include "constants.h"
#include "clause.h"
#include "decision.h"
#include "istrategy.h"
#include "problem_variable.h"
#include <fstream>

namespace solver
{
	class problem_solver
	{
	public:
		int index;
		std::string problem_name;
		std::vector<problem_variable> variables;
		std::vector<pdecision> decisions;
		std::string comments;

		decision_string solution;
		std::vector<decision_string *> conflicts;
		std::list<pdecision_string> unsolvable;

		bool solved;
		bool trace_enabled;
		int trace_index;
		bool trace_started;

		problem_solver()
		{
			clear();
		}

		~problem_solver()
		{
			clear();
		}

		void clear()
		{
			index = 0;
			solution.clear();
			problem_name.clear();
			variables.clear();
			comments.clear();
			for (int i = 0; i < decisions.size(); i++) 
			{
				delete decisions[i];
				decisions[i] = nullptr;
			}
			decisions.clear();
			solved = false;
			trace_enabled = false;
			trace_index = 0;
			trace_started = false;
		}

		bool solve(solver::istrategy& solver_strategy)
		{
			while (step());

			if (!solved)
			{
				solution.clear();
			}
			else
			{
				push_solution(solver_strategy);
			}

			return solved;
		}

		bool step()
		{
			bool finished = false;
			int s = decisions.size();

			if (build_conflict_string())
			{
				solved = true;
				finished = true;
			}
			else
			{
				solution.sort();
				add_conflict(solution);
				find_conflicts(solution);
				solved = false;
				finished = simplify_conflicts();
			}
		}

	private:

		void push_solution(solver::istrategy& solver_strategy)
		{
			int s = solution.size();
			int vc = variables.size();
			int i;
			int t;
			decision_char ch;

			for (i = 0; i < vc; i++)
			{
				auto& v = variables[i];
				v.check_valid = true;
				v.value = -1;
			}

			for (auto& ch : solution)
			{
				auto& v = variables[ch.lit.ref];
				t = solver_strategy.value_from_spin(ch.lit.spin);

				if (v.check_valid && (v.value == -1 || v.value == t))
				{
					v.value = t;
				}
				else
				{
					v.check_valid = false;
				}

				auto dec = decisions[ch.decision_idx];
				dec->selected_literal = -1;
				for (int i = 0; i < dec->literals.size(); i++)
				{
					if (ch.lit == dec->literals[i]) {
						dec->selected_literal = i;
						break;
					}
				}
			}
		}


		bool build_conflict_string(int idx)
		{
			solution.clear();
			int c = 0;
			int s = decisions.size();
			while (c < s) 
			{
				auto& dec = decisions[idx];
				if (!test_clause(dec)) 
				{
					return false;
				}
				c++;
				idx++;
				if (idx == s)
					idx = 0;
			}
			return true;
		}

		bool test_clause(pdecision dec)
		{
			for (auto lit : dec->literals)
			{
				if (solution.push_back(lit, dec->decision_idx))
				{
					if (check_conflict(solution))
					{
						return true;
					}
					else
					{
						solution.pop_back();
					}
				}
			}
			return false;
		}

		void find_conflicts(decision_string ds)
		{
			auto listi = ds.rbegin();
			if (listi != ds.rend())
			{
				listi++;
				if (listi != ds.rend())
				{
					decision_string dsnew = ds.remove_literal(listi->lit);
					bool r = check_conflict(dsnew);
					if (!r) 
					{
						add_conflict(dsnew);
						find_conflicts(dsnew);
					}
				}
			}
		}

		void add_conflict(decision_string ds)
		{
			bool found = false;
			int s = conflicts.size();
			for (int i = 0; i < s; i++) 
			{
				if (conflicts[i]->contains(ds)) {
					delete conflicts[i];
					conflicts[i] = ds.clone();
					found = true;
				}
			}
			if (!found) 
			{
				conflicts.push_back(ds.clone());
			}
		}

		bool check_conflict(decision_string& ds)
		{
			int s = decisions.size();
			for (int i = 0; i < s; i++)
			{
				auto dec = decisions[i];
				if (!ds.conflict_free(dec)) 
				{
					return false;
				}
			}
			return true;
		}

		struct ByDecision : public std::binary_function<pdecision_string, pdecision_string, bool>
		{
			bool operator()(const pdecision_string& lhs, const pdecision_string& rhs) const
			{
				return decision_string::compare( lhs, rhs );
			}
		};

		bool simplify_conflicts()
		{
			bool keep_looking = true;
			std::map<pdecision_string, std::list<pdecision_string>, ByDecision > decision_map;
			int s = conflicts.size();

			for (int i = 0; i < s; i++)
			{
				auto conf = conflicts[i];
				if (decision_map.count(conf) == 0) 
				{
					std::list<pdecision_string> new_list;
					decision_map[conf] = new_list;
				}

				auto& vlist = decision_map[conf];

				// we get rid of all the duplicates here
				// one, for cleanliness, and two,
				// 

				bool found = false;

				for (auto& item : vlist) 
				{
					if (item == conf)
						found = true;
				}

				if (!found) {
					vlist.push_back(conf);
				}
			}

			decision_map.clear();

			// now check for a clause that is unsatisfiable
			for (auto it = decision_map.begin(); it != decision_map.end(); ++it) 
			{
				int nbr_elements = it->second.size();
				int max_elements = 1 << it->first->size();
				if (nbr_elements == max_elements) {
					keep_looking = false;
					for (auto& item : it->second) {
						unsolvable.push_back(item);
					}
					break;
				}
			}

			return keep_looking;
		}
	};
}
